Nuprl Lemma : update_wf
11,40
postcript
pdf
A
,
B
:Type,
eq
:(
A
A
),
f
:(
A
B
),
x
:
A
,
v
:
B
.
f
[
x
:=
v
]
A
B
latex
Definitions
x
:
A
.
B
(
x
)
,
t
T
,
f
[
x
:=
v
]
Lemmas
ifthenelse
wf
,
bool
wf
origin
A, B:Type, eq:(A
A
), f:(AB), x:A, v:B. f[x:=v] 
AB A, B:Type, eq:(AA), f:(AB), x:A, v:B. f[x:=v] AB x:A. B(x) T